Inference at * 1 
Iof proof for Lemma eq int eq true elim sqequal:



1. i : 
2. j : 
  ((i = j) ~ tt)  (i = j) 

latex

 by D 0 

latex

 1: 

 1: 3. (i = j) ~ tt
 1:   i = j
 2: .....wf..... NILNIL

 2:   ((i = j) ~ tt)  Type
 .

Definitions

P  Q, t  T